Lambda the Ultimate

A Syntactic Approach to Type Soundness (1992) Andrew K. Wright, Matthias Felleisen.

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features.

This paper does a good job of explaining the foundations of type soundness. It has been previously discussed on the forums. I'm posting it here since I'm just discovering it for the first time, and I think it would be useful for other neophytes.

I am using the "[Redux]" tag to denote front page posts which revisit older papers, tutorials, or overview paper directed at less experienced members of LtU. Feel free to send me any suggestions for the series at cdiggins @ gmail.com.

The PVS Specification and Verification System from SRI is being released as open source.

Also coming with version 4.0 is the PVS wiki.

Self-Reproducing Programs in Common Lisp by Peter Norvig, 1990.

This paper reviews the classic self-reproducing expressions in Lisp, and presents some new ones that are unique to Common Lisp.

T: A Dialect of Lisp, or, LAMBDA: The Ultimate Software Tool

The T project is an experiment in language design and implementation.
Its purpose is to test the thesis developed by Steele and Sussman in
their series of papers about the Scheme language: that Scheme may be
used as the basis for a practical programming language of exceptional
expressive power; and, that implementations of scheme could perform
better than other Lisp systems, and competitively with implementations of programming languages, such as C and Bliss, which are usually
considered to be inherently more efficient than Lisp on conventional
machine architectures. We are developing a portable implementation of
T, currently targetted fo rthe VAX under the Unix and VMS operating
systems and for the Apollo, a MC68000-based workstations.

Chris Double has written a wonderfully concise example of parser combinators in Factor. Slava Pestov's Factor continues to be one of the most interesting language projects in development, in that it's both elegant and already has a solid set of tools.

Ralph Johnson mentions an interesting project from Pavel Krivanek to modularize Squeak. For example, there's a KernelImage that excludes the GUI (it's 2.8 MB compared to 15 MB for the full 3.9 release). The modularized images are created automatically from the complete image, by Squeak code.

It's been awhile since we discussed Squeak, which remains as far as I can tell, an interesting project worth keeping an eye on.

Like math puzzles and physics puzzles, there are many different kinds of programming puzzles. One way to classify programming puzzles is by the skills they exercise or the concepts they illustrate: knowledge of a language, designing a new algorithm, understanding a specification, etc.

On LtU, I'm interested in puzzles that are not specific to a language yet rely on a PL notion. Here's one attempt of mine, inspired by my student Jun Dai:

Your stair-climbing robot has a very simple low-level API: the "step" function takes no argument and attempts to climb one step as a side effect. Unfortunately, sometimes the attempt fails and the robot clumsily falls one step instead. The "step" function detects what happens and returns a boolean flag: true on success, false on failure. Write a function "step_up" that climbs one step up (by repeating "step" attempts if necessary). Assume that the robot is not already at the top of the stairs, and neither does it ever reach the bottom of the stairs. How small can you make "step_up"? Can you avoid using variables (even immutable ones) and numbers?

What do you think? What is your solution? How are the solutions related to each other? (If "step" fails with a fixed probability, then how many times does "step_up" expect to call "step"?)

More importantly, what is your favorite PL puzzle that is not (terribly) language-specific?

"... As the Erlang DCC is less than a quarter of the size of a similar C++/CORBA implementation, the product development in Erlang should be fast, and the code maintainable. We conclude that Erlang and associated libraries are suitable for the rapid development of maintainable and highly reliable distributed products."

Are High-level Languages suitable for Robust Telecoms Software? (pdf) also High-Level Techniques for Distributed Telecommunications Software

A Garbage-Collecting Typed Assembly Language. Chris Hawblitzel; Heng Huang; Lea Wittie; Juan Chen.

Abstract Typed assembly languages usually support heap allocation safely, but often rely on an external garbage collector to deallocate objects from the heap and prevent unsafe dangling pointers. Even if the external garbage collector is provably correct, verifying the safety of the interaction between TAL programs and garbage collection is nontrivial. This paper introduces a typed assembly language whose type system is expressive enough to type-check a Cheney-queue copying garbage collector, so that ordinary programs and garbage collection can co-exist and interact inside a single typed language. The only built-in types for memory are linear types describing individual memory words, so that TAL programmers can define their own object layouts, method table layouts, heap layouts, and memory management techniques.

The TAL-GC proofs can be found here.

Reform Prolog is a recursion-parallel implementation of Prolog. By executing all invocations of a recursive predicate in parallel, data-parallelism can be exploited. In contrast to most other parallel Prolog systems, Reform Prolog thus exploits structured parallelism; in contrast to present-day parallel Fortran systems, Reform Prolog can parallelize programs with procedure calls, pointer datastructures and arbitrary data dependences into doacross-style loops.

The Reform Prolog project ended in 1996 and somehow morphed into the High Performance Erlang project (which should be no surprise, as Erlang has clear roots in the Prolog world, though the concurrency model is different).